YES 1.55
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isPrefixOf :: Eq a => [Maybe a] -> [Maybe a] -> Bool) :: Eq a => [Maybe a] -> [Maybe a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isPrefixOf :: Eq a => [Maybe a] -> [Maybe a] -> Bool) :: Eq a => [Maybe a] -> [Maybe a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isPrefixOf :: Eq a => [Maybe a] -> [Maybe a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy1100), Succ(xy4001000)) → new_primPlusNat(xy1100, xy4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy1100), Succ(xy4001000)) → new_primPlusNat(xy1100, xy4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy300100), Succ(xy400100)) → new_primMulNat(xy300100, Succ(xy400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy300100), Succ(xy400100)) → new_primMulNat(xy300100, Succ(xy400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy30000), Succ(xy40000)) → new_primEqNat(xy30000, xy40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy30000), Succ(xy40000)) → new_primEqNat(xy30000, xy40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_@2, cc), cd), ce) → new_esEs(xy3000, xy4000, cc, cd)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(app(ty_@3, bcg), bch), bda)), hf), bbb)) → new_esEs2(xy3000, xy4000, bcg, bch, bda)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_@2, gd), ge)) → new_esEs(xy3000, xy4000, gd, ge)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_Maybe, de), ce) → new_esEs3(xy3000, xy4000, de)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(ty_Maybe, bag)) → new_esEs3(xy3002, xy4002, bag)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_[], bcf)), hf), bbb)) → new_esEs1(xy3000, xy4000, bcf)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(ty_Either, bd), be)) → new_esEs0(xy3001, xy4001, bd, be)
new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(ty_[], ec)), dh)) → new_esEs1(xy3000, xy4000, ec)
new_esEs0(Left(xy3000), Left(xy4000), app(app(ty_@2, df), dg), dh) → new_esEs(xy3000, xy4000, df, dg)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(app(ty_@3, db), dc), dd)), ce)) → new_esEs2(xy3000, xy4000, db, dc, dd)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_Either, cf), cg), ce) → new_esEs0(xy3000, xy4000, cf, cg)
new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(ty_Either, fc), fd))) → new_esEs0(xy3000, xy4000, fc, fd)
new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(ty_Either, fc), fd)) → new_esEs0(xy3000, xy4000, fc, fd)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(ty_Either, bd), be))) → new_esEs0(xy3001, xy4001, bd, be)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(ty_[], bf)) → new_esEs1(xy3001, xy4001, bf)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_@2, bcb), bcc)), hf), bbb)) → new_esEs(xy3000, xy4000, bcb, bcc)
new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(ty_@2, df), dg)), dh)) → new_esEs(xy3000, xy4000, df, dg)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_Maybe, de)), ce)) → new_esEs3(xy3000, xy4000, de)
new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(app(ty_@3, fg), fh), ga)) → new_esEs2(xy3000, xy4000, fg, fh, ga)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(ty_Either, gf), gg))) → new_esEs0(xy3000, xy4000, gf, gg)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(xy3001, xy4001, bb, bc)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_Either, cf), cg)), ce)) → new_esEs0(xy3000, xy4000, cf, cg)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs2(xy3000, xy4000, db, dc, dd)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(ty_[], bac)) → new_esEs1(xy3002, xy4002, bac)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bcb), bcc), hf, bbb) → new_esEs(xy3000, xy4000, bcb, bcc)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_[], bcf), hf, bbb) → new_esEs1(xy3000, xy4000, bcf)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(app(ty_@3, bad), bae), baf))) → new_esEs2(xy3002, xy4002, bad, bae, baf)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(ty_@2, hg), hh))) → new_esEs(xy3002, xy4002, hg, hh)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(app(ty_@3, ha), hb), hc)) → new_esEs2(xy3000, xy4000, ha, hb, hc)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_Maybe, hd)) → new_esEs3(xy3000, xy4000, hd)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(ty_Either, baa), bab)) → new_esEs0(xy3002, xy4002, baa, bab)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_Either, bcd), bce)), hf), bbb)) → new_esEs0(xy3000, xy4000, bcd, bce)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(app(ty_@3, bad), bae), baf)) → new_esEs2(xy3002, xy4002, bad, bae, baf)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(ty_[], bbe)), bbb)) → new_esEs1(xy3001, xy4001, bbe)
new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(app(ty_@3, ed), ee), ef)), dh)) → new_esEs2(xy3000, xy4000, ed, ee, ef)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bcg), bch), bda), hf, bbb) → new_esEs2(xy3000, xy4000, bcg, bch, bda)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(app(ty_@3, bg), bh), ca))) → new_esEs2(xy3001, xy4001, bg, bh, ca)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_Maybe, bdb)), hf), bbb)) → new_esEs3(xy3000, xy4000, bdb)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(ty_Maybe, bca), bbb) → new_esEs3(xy3001, xy4001, bca)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(ty_@2, bah), bba)), bbb)) → new_esEs(xy3001, xy4001, bah, bba)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_[], da), ce) → new_esEs1(xy3000, xy4000, da)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(ty_Maybe, cb))) → new_esEs3(xy3001, xy4001, cb)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(ty_@2, gd), ge))) → new_esEs(xy3000, xy4000, gd, ge)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bcd), bce), hf, bbb) → new_esEs0(xy3000, xy4000, bcd, bce)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(ty_[], bf))) → new_esEs1(xy3001, xy4001, bf)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), gc) → new_esEs1(xy3001, xy4001, gc)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(ty_[], bbe), bbb) → new_esEs1(xy3001, xy4001, bbe)
new_esEs0(Left(xy3000), Left(xy4000), app(ty_Maybe, eg), dh) → new_esEs3(xy3000, xy4000, eg)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_[], gh)) → new_esEs1(xy3000, xy4000, gh)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(ty_Either, baa), bab))) → new_esEs0(xy3002, xy4002, baa, bab)
new_esEs0(Left(xy3000), Left(xy4000), app(app(app(ty_@3, ed), ee), ef), dh) → new_esEs2(xy3000, xy4000, ed, ee, ef)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(ty_Maybe, hd))) → new_esEs3(xy3000, xy4000, hd)
new_esEs0(Left(xy3000), Left(xy4000), app(app(ty_Either, ea), eb), dh) → new_esEs0(xy3000, xy4000, ea, eb)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(ty_Maybe, cb)) → new_esEs3(xy3001, xy4001, cb)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(ty_[], bac))) → new_esEs1(xy3002, xy4002, bac)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(ty_Maybe, bca)), bbb)) → new_esEs3(xy3001, xy4001, bca)
new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(app(ty_@3, bg), bh), ca)) → new_esEs2(xy3001, xy4001, bg, bh, ca)
new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(ty_Maybe, eg)), dh)) → new_esEs3(xy3000, xy4000, eg)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(ty_Either, bbc), bbd)), bbb)) → new_esEs0(xy3001, xy4001, bbc, bbd)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(ty_@2, bb), bc))) → new_esEs(xy3001, xy4001, bb, bc)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(ty_Maybe, bag))) → new_esEs3(xy3002, xy4002, bag)
new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_Either, gf), gg)) → new_esEs0(xy3000, xy4000, gf, gg)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], gc)) → new_esEs1(xy3001, xy4001, gc)
new_esEs0(Right(xy3000), Right(xy4000), eh, app(ty_[], ff)) → new_esEs1(xy3000, xy4000, ff)
new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(app(ty_@3, fg), fh), ga))) → new_esEs2(xy3000, xy4000, fg, fh, ga)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_[], da)), ce)) → new_esEs1(xy3000, xy4000, da)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(app(ty_@3, bbf), bbg), bbh), bbb) → new_esEs2(xy3001, xy4001, bbf, bbg, bbh)
new_esEs0(Left(xy3000), Left(xy4000), app(ty_[], ec), dh) → new_esEs1(xy3000, xy4000, ec)
new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(ty_Either, ea), eb)), dh)) → new_esEs0(xy3000, xy4000, ea, eb)
new_esEs3(Just(xy300), Just(xy400), app(ty_Maybe, bdc)) → new_esEs3(xy300, xy400, bdc)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bdb), hf, bbb) → new_esEs3(xy3000, xy4000, bdb)
new_esEs0(Right(xy3000), Right(xy4000), eh, app(ty_Maybe, gb)) → new_esEs3(xy3000, xy4000, gb)
new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(ty_Maybe, gb))) → new_esEs3(xy3000, xy4000, gb)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(ty_@2, bah), bba), bbb) → new_esEs(xy3001, xy4001, bah, bba)
new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(ty_@2, fa), fb))) → new_esEs(xy3000, xy4000, fa, fb)
new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(app(ty_@3, bbf), bbg), bbh)), bbb)) → new_esEs2(xy3001, xy4001, bbf, bbg, bbh)
new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_@2, cc), cd)), ce)) → new_esEs(xy3000, xy4000, cc, cd)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(ty_Either, bbc), bbd), bbb) → new_esEs0(xy3001, xy4001, bbc, bbd)
new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(ty_@2, fa), fb)) → new_esEs(xy3000, xy4000, fa, fb)
new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(ty_@2, hg), hh)) → new_esEs(xy3002, xy4002, hg, hh)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(app(ty_@3, ha), hb), hc))) → new_esEs2(xy3000, xy4000, ha, hb, hc)
new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(ty_[], ff))) → new_esEs1(xy3000, xy4000, ff)
new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(ty_[], gh))) → new_esEs1(xy3000, xy4000, gh)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_@2, gd), ge)) → new_esEs(xy3000, xy4000, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_Maybe, hd)) → new_esEs3(xy3000, xy4000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(app(ty_@3, ha), hb), hc)) → new_esEs2(xy3000, xy4000, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(app(ty_Either, gf), gg)) → new_esEs0(xy3000, xy4000, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_@2, cc), cd), ce) → new_esEs(xy3000, xy4000, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(xy3001, xy4001, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_Maybe, de), ce) → new_esEs3(xy3000, xy4000, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(ty_Maybe, cb)) → new_esEs3(xy3001, xy4001, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(ty_[], bf)) → new_esEs1(xy3001, xy4001, bf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(ty_[], da), ce) → new_esEs1(xy3000, xy4000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs2(xy3000, xy4000, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(app(ty_@3, bg), bh), ca)) → new_esEs2(xy3001, xy4001, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), ba, app(app(ty_Either, bd), be)) → new_esEs0(xy3001, xy4001, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xy3000, xy3001), @2(xy4000, xy4001), app(app(ty_Either, cf), cg), ce) → new_esEs0(xy3000, xy4000, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bcb), bcc), hf, bbb) → new_esEs(xy3000, xy4000, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(ty_@2, bah), bba), bbb) → new_esEs(xy3001, xy4001, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(ty_@2, hg), hh)) → new_esEs(xy3002, xy4002, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_@2, bcb), bcc)), hf), bbb)) → new_esEs(xy3000, xy4000, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(ty_@2, df), dg)), dh)) → new_esEs(xy3000, xy4000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(ty_@2, hg), hh))) → new_esEs(xy3002, xy4002, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(ty_@2, bah), bba)), bbb)) → new_esEs(xy3001, xy4001, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(ty_@2, gd), ge))) → new_esEs(xy3000, xy4000, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(ty_@2, bb), bc))) → new_esEs(xy3001, xy4001, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(ty_@2, fa), fb))) → new_esEs(xy3000, xy4000, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_@2, cc), cd)), ce)) → new_esEs(xy3000, xy4000, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xy3000), Left(xy4000), app(app(ty_@2, df), dg), dh) → new_esEs(xy3000, xy4000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(ty_@2, fa), fb)) → new_esEs(xy3000, xy4000, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(ty_Maybe, bag)) → new_esEs3(xy3002, xy4002, bag)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(ty_Maybe, bca), bbb) → new_esEs3(xy3001, xy4001, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bdb), hf, bbb) → new_esEs3(xy3000, xy4000, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(ty_[], bac)) → new_esEs1(xy3002, xy4002, bac)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(ty_[], bcf), hf, bbb) → new_esEs1(xy3000, xy4000, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(ty_[], bbe), bbb) → new_esEs1(xy3001, xy4001, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(app(ty_@3, bad), bae), baf)) → new_esEs2(xy3002, xy4002, bad, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bcg), bch), bda), hf, bbb) → new_esEs2(xy3000, xy4000, bcg, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(app(ty_@3, bbf), bbg), bbh), bbb) → new_esEs2(xy3001, xy4001, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, hf, app(app(ty_Either, baa), bab)) → new_esEs0(xy3002, xy4002, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bcd), bce), hf, bbb) → new_esEs0(xy3000, xy4000, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(xy3000, xy3001, xy3002), @3(xy4000, xy4001, xy4002), he, app(app(ty_Either, bbc), bbd), bbb) → new_esEs0(xy3001, xy4001, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_Maybe, de)), ce)) → new_esEs3(xy3000, xy4000, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_Maybe, bdb)), hf), bbb)) → new_esEs3(xy3000, xy4000, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(ty_Maybe, cb))) → new_esEs3(xy3001, xy4001, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(ty_Maybe, hd))) → new_esEs3(xy3000, xy4000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(ty_Maybe, bca)), bbb)) → new_esEs3(xy3001, xy4001, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(ty_Maybe, eg)), dh)) → new_esEs3(xy3000, xy4000, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(ty_Maybe, bag))) → new_esEs3(xy3002, xy4002, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(xy300), Just(xy400), app(ty_Maybe, bdc)) → new_esEs3(xy300, xy400, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(ty_Maybe, gb))) → new_esEs3(xy3000, xy4000, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Left(xy3000), Left(xy4000), app(ty_Maybe, eg), dh) → new_esEs3(xy3000, xy4000, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy3000), Right(xy4000), eh, app(ty_Maybe, gb)) → new_esEs3(xy3000, xy4000, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(ty_[], bcf)), hf), bbb)) → new_esEs1(xy3000, xy4000, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(ty_[], ec)), dh)) → new_esEs1(xy3000, xy4000, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(ty_[], bbe)), bbb)) → new_esEs1(xy3001, xy4001, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(ty_[], bf))) → new_esEs1(xy3001, xy4001, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(ty_[], bac))) → new_esEs1(xy3002, xy4002, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], gc)) → new_esEs1(xy3001, xy4001, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(ty_[], da)), ce)) → new_esEs1(xy3000, xy4000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(ty_[], ff))) → new_esEs1(xy3000, xy4000, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(ty_[], gh))) → new_esEs1(xy3000, xy4000, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), gc) → new_esEs1(xy3001, xy4001, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(xy3000, xy3001), :(xy4000, xy4001), app(ty_[], gh)) → new_esEs1(xy3000, xy4000, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy3000), Right(xy4000), eh, app(ty_[], ff)) → new_esEs1(xy3000, xy4000, ff)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Left(xy3000), Left(xy4000), app(ty_[], ec), dh) → new_esEs1(xy3000, xy4000, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(app(ty_@3, bcg), bch), bda)), hf), bbb)) → new_esEs2(xy3000, xy4000, bcg, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(app(ty_@3, db), dc), dd)), ce)) → new_esEs2(xy3000, xy4000, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(app(ty_@3, bad), bae), baf))) → new_esEs2(xy3002, xy4002, bad, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(app(ty_@3, ed), ee), ef)), dh)) → new_esEs2(xy3000, xy4000, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(app(ty_@3, bg), bh), ca))) → new_esEs2(xy3001, xy4001, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(app(ty_@3, fg), fh), ga))) → new_esEs2(xy3000, xy4000, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(app(ty_@3, bbf), bbg), bbh)), bbb)) → new_esEs2(xy3001, xy4001, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(app(ty_@3, ha), hb), hc))) → new_esEs2(xy3000, xy4000, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(Right(xy3000)), Just(Right(xy4000)), app(app(ty_Either, eh), app(app(ty_Either, fc), fd))) → new_esEs0(xy3000, xy4000, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, ba), app(app(ty_Either, bd), be))) → new_esEs0(xy3001, xy4001, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(:(xy3000, xy3001)), Just(:(xy4000, xy4001)), app(ty_[], app(app(ty_Either, gf), gg))) → new_esEs0(xy3000, xy4000, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@2(xy3000, xy3001)), Just(@2(xy4000, xy4001)), app(app(ty_@2, app(app(ty_Either, cf), cg)), ce)) → new_esEs0(xy3000, xy4000, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, app(app(ty_Either, bcd), bce)), hf), bbb)) → new_esEs0(xy3000, xy4000, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), hf), app(app(ty_Either, baa), bab))) → new_esEs0(xy3002, xy4002, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(@3(xy3000, xy3001, xy3002)), Just(@3(xy4000, xy4001, xy4002)), app(app(app(ty_@3, he), app(app(ty_Either, bbc), bbd)), bbb)) → new_esEs0(xy3001, xy4001, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(Left(xy3000)), Just(Left(xy4000)), app(app(ty_Either, app(app(ty_Either, ea), eb)), dh)) → new_esEs0(xy3000, xy4000, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(app(ty_@3, fg), fh), ga)) → new_esEs2(xy3000, xy4000, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(Left(xy3000), Left(xy4000), app(app(app(ty_@3, ed), ee), ef), dh) → new_esEs2(xy3000, xy4000, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(xy3000), Right(xy4000), eh, app(app(ty_Either, fc), fd)) → new_esEs0(xy3000, xy4000, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(xy3000), Left(xy4000), app(app(ty_Either, ea), eb), dh) → new_esEs0(xy3000, xy4000, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3